Verifying properties of large sets of processes with network invariants,” in Automatic Verification Methods for Finite State Systems

If a system is built from a large number of identical finite-state processes, it seems intu-itively obvious that, with the help of "a little induction", the verification of such a system can be reduced to a finite-state problem. The difficulty is to find the right form of "a little induction". There have been several attempts to address this problem in the con-text of model-checking [CGBS6], [CGS7], [GSS7]. In very general terms (see Section 6 for more details), the approach is to find ways of proving that if a process atisfies a fornmla, then the n-fold parallel composition of this process with itself still satisfies the same (or a related) formula. This approach makes some interesting verifications possible. However, it has its limits and usually requires the implementation of special purpose tools. In this paper, we propose an alternative approach. It is an attempt o make the "little induction " explicit and simple. If one wants to prove that some property holds for the composition of n processes P, one ought to be able to proceed as follows. Prove that one process satisfies the property or, as is often necessary when using induction, a stronger property I. Then prove that the composition of any process satisfying I with one of the processes P still satisfies I. Such a property I essentially represents the joint behavior of any number of processes P. Since adding one more process P to a network satisfying I does not change I, we call it a network invariant. All this is general and quite obvious. The problem is to find a framework in which it works. For this, we turn to process theory in the style of CCS and CSP [MilS0], [Hoa85]. We actually use a variant of TCSP, but this choice is not important as long as some conditions made explicit in Section 2 are satisfied. The idea is that the network invariant I is itself expressed as a process. The inductive step then essentially reduces to proving in the process theory that I I I P is a process equal to or stronger than I. Of course if the processes are finite-state, this can be done with an automatic verification toot. Hence, once the invariant I is found, our method is completely automatic